a:rationals. -(-(a)) = a 

latex

Definitions	imon{i:l}, t  T, igrp{i:l}, t.2, t.1, prop{i:l}, P  Q, mon{i:l}, grp{i:l}, abgrp{i:l}, qadd_grp, grp_inv(g), grp_car(g), x:A. B(x)
Lemmas	abgrp wf, grp inv wf, inverse wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, grp inv inv